Inference at * 1 1 2 1 
Iof proof for Lemma complete nat ind with y:

.....assertion..... NILNIL

1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  !Void()!Void()
  n:. Y(f,x. g(x,f))  (m:n. P(m)) 

latex

 by ((D 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok 
C:t) inil_term))) 

latex

C1: 

C1: 4. n : 
C1:   Y(f,x. g(x,f))  (m:n. P(m))
C.

Definitions	t  T, x:A. B(x)
Lemmas	nat wf